(1) CpxTrsMatchBoundsProof (EQUIVALENT transformation)
A linear upper bound on the runtime complexity of the TRS R could be shown with a Match Bound [MATCHBOUNDS1,MATCHBOUNDS2] of 6.
The certificate found is represented by the following graph.
Start state: 2738
Accept states: [2740, 2742, 2743, 2744, 2745]
Transitions:
2738→2740[active_1|0]
2738→2742[proper_1|0]
2738→2743[f_1|0]
2738→2744[g_1|0]
2738→2745[top_1|0]
2738→2738[c|0, mark_1|0, ok_1|0]
2738→2746[c|1]
2738→2749[c|1]
2738→2750[f_1|1]
2738→2751[g_1|1]
2738→2752[active_1|1]
2738→2753[proper_1|1]
2738→2756[c|2]
2738→2762[c|2]
2738→2766[c|3]
2738→2778[c|4]
2746→2747[g_1|1]
2746→2760[proper_1|2]
2747→2748[f_1|1]
2747→2759[proper_1|2]
2748→2740[mark_1|1]
2748→2752[mark_1|1]
2748→2754[proper_1|2]
2749→2742[ok_1|1]
2749→2753[ok_1|1]
2749→2755[active_1|2]
2750→2743[ok_1|1]
2750→2750[ok_1|1]
2751→2744[ok_1|1]
2751→2751[ok_1|1]
2752→2745[top_1|1]
2753→2745[top_1|1]
2754→2745[top_1|2]
2755→2745[top_1|2]
2756→2757[g_1|2]
2756→2764[proper_1|3]
2757→2758[f_1|2]
2757→2763[proper_1|3]
2758→2755[mark_1|2]
2758→2761[proper_1|3]
2759→2754[f_1|2]
2760→2759[g_1|2]
2761→2745[top_1|3]
2762→2760[ok_1|2]
2762→2765[g_1|3]
2762→2770[g_1|4]
2762→2774[proper_1|5]
2763→2761[f_1|3]
2764→2763[g_1|3]
2765→2759[ok_1|3]
2765→2767[f_1|3]
2766→2764[ok_1|3]
2766→2768[g_1|4]
2766→2775[g_1|5]
2766→2774[ok_1|3]
2766→2777[proper_1|6]
2767→2754[ok_1|3]
2767→2769[active_1|3]
2768→2763[ok_1|4]
2768→2771[f_1|4]
2768→2772[ok_1|4]
2768→2779[active_1|5]
2769→2745[top_1|3]
2770→2769[mark_1|4]
2770→2772[proper_1|4]
2771→2761[ok_1|4]
2771→2773[active_1|4]
2772→2745[top_1|4]
2773→2745[top_1|4]
2774→2772[g_1|5]
2775→2773[mark_1|5]
2775→2776[proper_1|5]
2776→2745[top_1|5]
2777→2776[g_1|6]
2778→2777[ok_1|4]
2778→2780[g_1|5]
2779→2745[top_1|5]
2780→2776[ok_1|5]
2780→2781[active_1|6]
2781→2745[top_1|6]